p:FinProbSpace, n:, X:RandomVariable(p;n), a:. rv-disjoint(p;n;a;X) 

latex

Definitions	{x:A| B(x)} , , A  B, A, False, P  Q, rv-disjoint(p;n;X;Y), , RandomVariable(p;n), x:A. B(x), , t  T, FinProbSpace, left + right, Void, P  Q, <a, b>, , s = t, f(a), suptype(S; T), Type, #$n, rv-const(a), {i..j}, i  j < k, P & Q, S  T, x:AB(x), Outcome
Lemmas	p-outcome wf, int seg wf, not wf, finite-prob-space wf, nat wf, random-variable wf, rationals wf